T:Type, R:(TT).
Order(T;x,y.R(x,y))
 (x, y:T. Dec(x = y))
 (a, b:T. R(a,b)  (strict_part(x,y.R(x,y);a;b)  (a = b))) 

latex

Up	rel 1, rel 1
Definitions	x,y. t(x;y), t  T, P  Q, P & Q, strict_part(x,y.R(x;y);a;b), P  Q, P  Q, x(s1,s2), P  Q, , x:A. B(x), A, AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), Order(T;x,y.R(x;y)), Dec(P), False
Lemmas	order wf, decidable wf, not wf